Search for: All records

Increasingly more mobile browsers are developed to use proxies for traffic compression and censorship circumvention. While these browsers can offer such desirable features, their security implications are, however, not well understood, especially when tangled with TLS in the mix. Apart from vendor-specific proprietary designs, there are mainly 2 models of using proxies with browsers: TLS interception and HTTP tunneling. To understand the current practices employed by proxy-based mobile browsers, we analyze 34 Android browser apps that are representative of the ecosystem, and examine how their deployments are affecting communication security. Though the impacts of TLS interception on security was studied before in other contexts, proxy-based mobile browsers were not considered previously. In addition, the tunneling model requires the browser itself to enforce certain desired security policies (e.g., validating certificates and avoiding the use of weak cipher suites), and it is preferable to have such enforcement matching the security level of conventional desktop browsers. Our evaluation shows that many proxy-based mobile browsers downgrade the overall quality of TLS sessions, by for example allowing old versions of TLS (e.g., SSLv3.0 and TLSv1.0) and accepting weak cryptographic algorithms (e.g., 3DES and RC4) as well as unsatisfactory certificates (e.g., revoked or signed by untrusted CAs), thus exposing their users to potential security and privacy threats. We have reported our findings to the vendors of vulnerable proxy-based browsers and are waiting for their response. 

Abstract This paper focuses on protecting the cellular paging protocol — which balances between the quality-of-service and battery consumption of a device — against security and privacy attacks. Attacks against this protocol can have severe repercussions, for instance, allowing attacker to infer a victim’s location, leak a victim’s IMSI, and inject fabricated emergency alerts. To secure the protocol, we first identify the underlying design weaknesses enabling such attacks and then propose efficient and backward-compatible approaches to address these weaknesses. We also demonstrate the deployment feasibility of our enhanced paging protocol by implementing it on an open-source cellular protocol library and commodity hardware. Our evaluation demonstrates that the enhanced protocol can thwart attacks without incurring substantial overhead. 

This paper focuses on developing a security mechanism geared towards appified smart-home platforms. Such platforms often expose programming interfaces for developing automation apps that mechanize different tasks among smart sensors and actuators (e.g., automatically turning on the AC when the room temperature is above 80 F). Due to the lack of effective access control mechanisms, these automation apps can not only have unrestricted access to the user's sensitive information (e.g., the user is not at home) but also violate user expectations by performing undesired actions. As users often obtain these apps from unvetted sources, a malicious app can wreak havoc on a smart-home system by either violating the user's security and privacy, or creating safety hazards (e.g., turning on the oven when no one is at home). To mitigate such threats, we propose Expat which ensures that user expectations are never violated by the installed automation apps at runtime. To achieve this goal, Expat provides a platform-agnostic, formal specification language UEI for capturing user expectations of the installed automation apps' behavior. For effective authoring of these expectations (as policies) in UEI, Expat also allows a user to check the desired properties (e.g., consistency, entailment) of them; which due to their formal semantics can be easily discharged by an SMT solver. Expat then enforces UEI policies in situ with an inline reference monitor which can be realized using the same app programming interface exposed by the underlying platform. We instantiate Expat for one of the representative platforms, OpenHAB, and demonstrate it can effectively mitigate a wide array of threats by enforcing user expectations while incurring only modest performance overhead. 

We discuss how symbolic execution can be used to not only find low-level errors but also analyze the semantic correctness of protocol implementations. To avoid manually crafting test cases, we propose a strategy of meta-level search, which leverages constraints stemmed from the input formats to automatically generate concolic test cases. Additionally, to aid root-cause analysis, we develop constraint provenance tracking (CPT), a mechanism that associates atomic sub-formulas of path constraints with their corresponding source level origins. We demonstrate the power of symbolic analysis with a case study on PKCS#1 v1.5 signature verification. Leveraging meta-level search and CPT, we analyzed 15 recent open-source implementations using symbolic execution and found semantic flaws in 6 of them. Further analysis of these flaws showed that 4 implementations are susceptible to new variants of the Bleichenbacher low-exponent RSA signature forgery. One implementation suffers from potential denial of service attacks with purposefully crafted signatures. All our findings have been responsibly shared with the affected vendors. Among the flaws discovered, 6 new CVEs have been assigned to the immediately exploitable ones.